Inference at * 
Iof proof for Lemma spread to pi12:


  A:Type, B:(AType), p:(x:A  B(x)), C:Type, b:(x:AB(x)C).
  let x,y = p in b(x,y) = b(p.1,p.2) 

latex

 by ((UnivCD) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 1. A : Type
C1: 2. B : AType
C1: 3. p : x:A  B(x)
C1: 4. C : Type
C1: 5. b : x:AB(x)C
C1:   let x,y = p in b(x,y) = b(p.1,p.2)
C.

Definitions

t  T, x(s), x:A. B(x)